『Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages』

1. どんなもの？

2. 先行研究と比べてどこがすごい？

他の定理証明支援系のマクロより衛生的で使いやすいマクロシステムを実装した

3. 技術や手法のキモはどこ？

Schemeのマクロシステムを参考にした衛生的なマクロアルゴリズム

4. どうやって有効だと検証した？

実装して確認した？

5. 議論はある？

6. 次に読むべき論文は？

table:訳

Interactive Theorem Proving(ITP) 対話的定理証明支援系

not only A but B AだけでなくBも

rudimentary 初歩的な

counterintuitive 常識［直観］に反する［そぐわない］

terse 簡単な、明瞭な

statically 静的な

vice versa 逆も同様に

syntactic category 文法的範疇、構文カテゴリ

type-aware elaboration 型を意識した精緻化？

elaboration 精緻化？、エラボレーション？

right-hand side 右辺

1. Introduction

Mixfix notation systems

Lispはマクロで構文木を返す？

infixr, infixl

パターンベース、手続き的なベース

2. The New Macro System

code:memo

macro "defthunk" id:ident ":=" e:term : command =>

`(def $id := Thunk.mk (fun _ => $e))

defthunk big := mkArray 100000 true

code:memo

syntax term "`" term ":" term : term

macro_rules

\`()

準クオート(quasiquotation)

$

アンクォート(論文中ではanti-quotation)

code:lisp

;; ref: On Lisp 2. 変数捕捉と多重評価

(defmacro for ((var start stop) &body body)

(let ((gstop (gensym)))

`(do ((,var ,start (1+ ,var)) (,gstop ,stop)) ((>= ,var ,gstop))

,@body)))

code:memo

マクロシステムが洗練されていないため12個も似たようなマクロを定義しないといけない

3. Hygiene Algorithm

table:訳

conventional 従来の

elaborator エラボレーター？精緻化器...? 推敲器...?

syntax quotation

subsequent その後の

macro expander マクロ展開器

マクロの展開前にスコープの設定をしないといけない

Expantion Algorithm

マクロ展開器がマクロを全部展開する

これ以上展開できないのはcore forms

n.msc1.msc2.. . ..mscn{tsc1,. . .,tscn}

n: オリジナル名称

msc: マクロスコープ

tsc: トップレベルスコープ

グローバルコンテキスト(globbal context)

ローカルコンテキスト(local context)

4. Implementation

table:訳

identifiers 識別子

構文オブジェクト(Syntax object)

リテラルとは、プログラムのソースコードにおいて使用される、数値や文字列を直接に記述した定数のことである。

TransformerM monad

TransformerM Syntax where the TransformerM monad gives access to the global context and a fresh macro scope per macro expansion

ExpanderM monad

5. Integrating Macros into Elaboration

6. Tactic Hygiene

7. Best-Effort Eager Name Analysis in Macros

8. Related Work

9. Conclusion

参考